LeanDojo
lean
ML
webapp
This was posted a while back on the Lean Zulip:
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
According to their description, LeanDojo is an open-source Lean playground consisting of toolkits, data, models, and benchmarks. Plus they also provide an LLM-based prover and a chatGPT plugin. All of this looks amazing and something worth learning more about.